Nuprl Lemma : es-tg-sends_wf
11,40
postcript
pdf
the_es
:ES,
e
:E,
l
:IdLnk,
tg
:Id. sends(
l
,
tg
,
e
)
((Msg on
l
) List)
latex
Definitions
t
T
,
{
x
:
A
|
B
(
x
)}
,
(Msg on
l
)
,
ES
,
x
:
A
.
B
(
x
)
,
E
,
IdLnk
,
Id
,
Msg
,
x
:
A
B
(
x
)
,
sends(
l
;
e
)
,
mtag(
m
)
,
a
=
b
,
x
.
A
(
x
)
,
filter(
P
;
l
)
,
sends(
l
,
tg
,
e
)
Lemmas
filter
wf
,
eq
id
wf
,
es-mtag
wf
,
es-Msgl
wf
,
es-sends
wf
,
Id
wf
,
IdLnk
wf
,
es-E
wf
,
event
system
wf
origin
the_es:ES, e:E, l:IdLnk, tg:Id. sends(l,tg,e) 
((Msg on l) List) the_es:ES, e:E, l:IdLnk, tg:Id. sends(l,tg,e) ((Msg on l) List) Tx:A. B(x)
B(x)
x.A(x)